COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 unify.lsp[s84,jmc]	Unification algorithm
C00004 ENDMK
C⊗;
;;; unify.lsp[s84,jmc]	Unification algorithm

(defun unify (e1 e2 a)
       (cond
	((eq a 'no) 'no)
	((isconst e1)
	 (if (isconst e2)
	     (if (equal e1 e2) a 'no)
	     (unify e2 e1 a)))
	((isvar e1)
	 (let ((e1a (assoc e1 a)))
	      (if
	       (null e1a)
	       (push (cons e1 e2) a)
	       (unify e1a e2 a))))
	((isconst e2) 'no)
	((isvar e2)
	 (let ((e2a (assoc e2 a)))
	      (if
	       (null e2a)
	       (push (cons e2 e1) a)
	       (unify e2a e1 a))))
	(t (unify (cdr e1) (cdr e2) (unify (car e1) (car e2) a)))))

(defun isvar (e) (memq e '(x x0 x1 x2 y y0 y1 y2 z z0 z1 z2)))

(defun isconst (e)
       (if (atom e)
	   (not (isvar e))
	   (eq (car e) 'quote)
))

(unify 'a 'b nil)

(unify 'x 'a nil)

(unify '(f a) '(g a) nil)

(unify '(f a) '(f a) nil)

(unify '(f x) '(f a) nil)

(unify '(f x (g a)) '(f (h b) y) nil)